(set-logic QF_UFLIA)
(set-info :source |
  These benchmarks were obtained from the KIND tool during verification of
  Lustre programs.  See also the lustre family of benchmarks in QF_LIA.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (<= 0 _n))
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Int)
(declare-fun ___z7z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Bool)
(declare-fun ___z9z___ (Int) Bool)
(push 1)
(assert (= (= (___z5z___ 0) (___z4z___ 0)) (___z3z___ 0)))
(assert (= (___z4z___ 0) (= (___z6z___ 0) 5)))
(assert (= (___z5z___ 0) (and (___z9z___ 0) (___z7z___ 0))))
(assert (let ((?v_0 (___z6z___ (- 1)))) (= (___z6z___ 0) (ite (= _base 0) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base 0))) (= (___z7z___ 0) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 1))))))))
(assert (let ((?v_0 (= _base 0)) (?v_1 (___z7z___ (- 1))) (?v_2 (___z8z___ (- 1)))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 1)))))))) (___z8z___ 0))))
(assert (let ((?v_0 (= _base 0)) (?v_1 (___z7z___ (- 1)))) (= (___z9z___ 0) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 1))) (and (not ?v_1) (___z9z___ (- 1)))))))))
(assert (= (= (___z5z___ (- 1)) (___z4z___ (- 1))) (___z3z___ (- 1))))
(assert (= (= (___z6z___ (- 1)) 5) (___z4z___ (- 1))))
(assert (= (___z5z___ (- 1)) (and (___z7z___ (- 1)) (___z9z___ (- 1)))))
(assert (let ((?v_0 (___z6z___ (- 2)))) (= (___z6z___ (- 1)) (ite (= _base (- 1)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 1)))) (= (___z7z___ (- 1)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 2))))))))
(assert (let ((?v_0 (= _base (- 1))) (?v_1 (___z7z___ (- 2))) (?v_2 (___z8z___ (- 2)))) (= (___z8z___ (- 1)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 2)))))))))))
(assert (let ((?v_0 (= _base (- 1))) (?v_1 (___z7z___ (- 2)))) (= (___z9z___ (- 1)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 2))) (and (not ?v_1) (___z9z___ (- 2)))))))))
(push 1)
(assert (not (or (not (= _base (- 1))) (and (___z3z___ 0) (___z3z___ (- 1))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 1)))
(assert (___z3z___ (- 2)))
(push 1)
(assert (= (= (___z5z___ _n) (___z4z___ _n)) (___z3z___ _n)))
(assert (= (___z4z___ _n) (= (___z6z___ _n) 5)))
(assert (= (___z5z___ _n) (and (___z9z___ _n) (___z7z___ _n))))
(assert (let ((?v_0 (___z6z___ (+ _n (- 1))))) (= (___z6z___ _n) (ite (= _n _base) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _n _base))) (= (___z7z___ _n) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ _n (- 1)))))))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (+ _n (- 1)))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ _n)))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (+ _n (- 1)))) (let ((?v_2 (___z7z___ ?v_1))) (= (___z9z___ _n) (and (not ?v_0) (or ?v_0 (or (and ?v_2 (___z8z___ ?v_1)) (and (not ?v_2) (___z9z___ ?v_1)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z5z___ ?v_0) (___z4z___ ?v_0)) (___z3z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z6z___ ?v_0) 5) (___z4z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z5z___ ?v_0) (and (___z7z___ ?v_0) (___z9z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2)) (?v_4 (___z8z___ ?v_2))) (= (___z8z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and (not ?v_3) ?v_4) (and ?v_3 (and (not ?v_4) (not (___z9z___ ?v_2))))))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (___z3z___ (+ _n (- 1))))
(assert (not (or (not (= _base (- 1))) (___z3z___ _n))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 1))))
(assert (___z3z___ (+ _n (- 2))))
(assert (= (___z3z___ (- 2)) (= (___z5z___ (- 2)) (___z4z___ (- 2)))))
(assert (= (= (___z6z___ (- 2)) 5) (___z4z___ (- 2))))
(assert (= (___z5z___ (- 2)) (and (___z7z___ (- 2)) (___z9z___ (- 2)))))
(assert (let ((?v_0 (___z6z___ (- 3)))) (= (___z6z___ (- 2)) (ite (= _base (- 2)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 2)))) (= (___z7z___ (- 2)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 3))))))))
(assert (let ((?v_0 (= _base (- 2))) (?v_1 (___z7z___ (- 3))) (?v_2 (___z8z___ (- 3)))) (= (___z8z___ (- 2)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 3)))))))))))
(assert (let ((?v_0 (= _base (- 2))) (?v_1 (___z7z___ (- 3)))) (= (___z9z___ (- 2)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 3))) (and (not ?v_1) (___z9z___ (- 3)))))))))
(assert (= (= (___z5z___ _n) (___z4z___ _n)) (___z3z___ _n)))
(assert (= (___z4z___ _n) (= (___z6z___ _n) 5)))
(assert (= (___z5z___ _n) (and (___z9z___ _n) (___z7z___ _n))))
(assert (let ((?v_0 (___z6z___ (+ _n (- 1))))) (= (___z6z___ _n) (ite (= _n _base) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _n _base))) (= (___z7z___ _n) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ _n (- 1)))))))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (+ _n (- 1)))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ _n)))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (+ _n (- 1)))) (let ((?v_2 (___z7z___ ?v_1))) (= (___z9z___ _n) (and (not ?v_0) (or ?v_0 (or (and ?v_2 (___z8z___ ?v_1)) (and (not ?v_2) (___z9z___ ?v_1)))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 2))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 3)))
(push 1)
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z5z___ ?v_0) (___z4z___ ?v_0)) (___z3z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z6z___ ?v_0) 5) (___z4z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z5z___ ?v_0) (and (___z7z___ ?v_0) (___z9z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2)) (?v_4 (___z8z___ ?v_2))) (= (___z8z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and (not ?v_3) ?v_4) (and ?v_3 (and (not ?v_4) (not (___z9z___ ?v_2))))))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 2) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 2))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 3))))
(assert (= (___z3z___ (- 3)) (= (___z5z___ (- 3)) (___z4z___ (- 3)))))
(assert (= (= (___z6z___ (- 3)) 5) (___z4z___ (- 3))))
(assert (= (___z5z___ (- 3)) (and (___z7z___ (- 3)) (___z9z___ (- 3)))))
(assert (let ((?v_0 (___z6z___ (- 4)))) (= (___z6z___ (- 3)) (ite (= _base (- 3)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 3)))) (= (___z7z___ (- 3)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 4))))))))
(assert (let ((?v_0 (= _base (- 3))) (?v_1 (___z7z___ (- 4))) (?v_2 (___z8z___ (- 4)))) (= (___z8z___ (- 3)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 4)))))))))))
(assert (let ((?v_0 (= _base (- 3))) (?v_1 (___z7z___ (- 4)))) (= (___z9z___ (- 3)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 4))) (and (not ?v_1) (___z9z___ (- 4)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z5z___ ?v_0) (___z4z___ ?v_0)) (___z3z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z6z___ ?v_0) 5) (___z4z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z5z___ ?v_0) (and (___z7z___ ?v_0) (___z9z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2)) (?v_4 (___z8z___ ?v_2))) (= (___z8z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and (not ?v_3) ?v_4) (and ?v_3 (and (not ?v_4) (not (___z9z___ ?v_2))))))))))))
(assert (let ((?v_1 (+ _n (- 1))) (?v_0 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 3))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 4)))
(push 1)
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 2) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 3) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 3))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 4))))
(assert (= (___z3z___ (- 4)) (= (___z5z___ (- 4)) (___z4z___ (- 4)))))
(assert (= (= (___z6z___ (- 4)) 5) (___z4z___ (- 4))))
(assert (= (___z5z___ (- 4)) (and (___z7z___ (- 4)) (___z9z___ (- 4)))))
(assert (let ((?v_0 (___z6z___ (- 5)))) (= (___z6z___ (- 4)) (ite (= _base (- 4)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 4)))) (= (___z7z___ (- 4)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 5))))))))
(assert (let ((?v_0 (= _base (- 4))) (?v_1 (___z7z___ (- 5))) (?v_2 (___z8z___ (- 5)))) (= (___z8z___ (- 4)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 5)))))))))))
(assert (let ((?v_0 (= _base (- 4))) (?v_1 (___z7z___ (- 5)))) (= (___z9z___ (- 4)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 5))) (and (not ?v_1) (___z9z___ (- 5)))))))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 2)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 2)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 2) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 2))) (?v_0 (= (+ _n (* (- 1) _base)) 2))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 4))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 5)))
(push 1)
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 3) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 4) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 4))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 5))))
(assert (= (___z3z___ (- 5)) (= (___z5z___ (- 5)) (___z4z___ (- 5)))))
(assert (= (= (___z6z___ (- 5)) 5) (___z4z___ (- 5))))
(assert (= (___z5z___ (- 5)) (and (___z7z___ (- 5)) (___z9z___ (- 5)))))
(assert (let ((?v_0 (___z6z___ (- 6)))) (= (___z6z___ (- 5)) (ite (= _base (- 5)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 5)))) (= (___z7z___ (- 5)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 6))))))))
(assert (let ((?v_0 (= _base (- 5))) (?v_1 (___z7z___ (- 6))) (?v_2 (___z8z___ (- 6)))) (= (___z8z___ (- 5)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 6)))))))))))
(assert (let ((?v_0 (= _base (- 5))) (?v_1 (___z7z___ (- 6)))) (= (___z9z___ (- 5)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 6))) (and (not ?v_1) (___z9z___ (- 6)))))))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 3)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 3)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 3) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 3))) (?v_0 (= (+ _n (* (- 1) _base)) 3))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 5))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 6)))
(push 1)
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 4) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 5) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 5))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 6))))
(assert (= (___z3z___ (- 6)) (= (___z5z___ (- 6)) (___z4z___ (- 6)))))
(assert (= (= (___z6z___ (- 6)) 5) (___z4z___ (- 6))))
(assert (= (___z5z___ (- 6)) (and (___z7z___ (- 6)) (___z9z___ (- 6)))))
(assert (let ((?v_0 (___z6z___ (- 7)))) (= (___z6z___ (- 6)) (ite (= _base (- 6)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 6)))) (= (___z7z___ (- 6)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 7))))))))
(assert (let ((?v_0 (= _base (- 6))) (?v_1 (___z7z___ (- 7))) (?v_2 (___z8z___ (- 7)))) (= (___z8z___ (- 6)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 7)))))))))))
(assert (let ((?v_0 (= _base (- 6))) (?v_1 (___z7z___ (- 7)))) (= (___z9z___ (- 6)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 7))) (and (not ?v_1) (___z9z___ (- 7)))))))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 4)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 4)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 4) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 4))) (?v_0 (= (+ _n (* (- 1) _base)) 4))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 6))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 7)))
(push 1)
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 5) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 6) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 6))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 7))))
(assert (= (___z3z___ (- 7)) (= (___z5z___ (- 7)) (___z4z___ (- 7)))))
(assert (= (= (___z6z___ (- 7)) 5) (___z4z___ (- 7))))
(assert (= (___z5z___ (- 7)) (and (___z7z___ (- 7)) (___z9z___ (- 7)))))
(assert (let ((?v_0 (___z6z___ (- 8)))) (= (___z6z___ (- 7)) (ite (= _base (- 7)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 7)))) (= (___z7z___ (- 7)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 8))))))))
(assert (let ((?v_0 (= _base (- 7))) (?v_1 (___z7z___ (- 8))) (?v_2 (___z8z___ (- 8)))) (= (___z8z___ (- 7)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 8)))))))))))
(assert (let ((?v_0 (= _base (- 7))) (?v_1 (___z7z___ (- 8)))) (= (___z9z___ (- 7)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 8))) (and (not ?v_1) (___z9z___ (- 8)))))))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 5)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 5)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 5) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 5))) (?v_0 (= (+ _n (* (- 1) _base)) 5))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 7))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 8)))
(push 1)
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 6) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 7) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 7))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 8))))
(assert (= (___z3z___ (- 8)) (= (___z5z___ (- 8)) (___z4z___ (- 8)))))
(assert (= (= (___z6z___ (- 8)) 5) (___z4z___ (- 8))))
(assert (= (___z5z___ (- 8)) (and (___z7z___ (- 8)) (___z9z___ (- 8)))))
(assert (let ((?v_0 (___z6z___ (- 9)))) (= (___z6z___ (- 8)) (ite (= _base (- 8)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 8)))) (= (___z7z___ (- 8)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 9))))))))
(assert (let ((?v_0 (= _base (- 8))) (?v_1 (___z7z___ (- 9))) (?v_2 (___z8z___ (- 9)))) (= (___z8z___ (- 8)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 9)))))))))))
(assert (let ((?v_0 (= _base (- 8))) (?v_1 (___z7z___ (- 9)))) (= (___z9z___ (- 8)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 9))) (and (not ?v_1) (___z9z___ (- 9)))))))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 6)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 6)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 6) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 6))) (?v_0 (= (+ _n (* (- 1) _base)) 6))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 8))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 9)))
(push 1)
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 7) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 8) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 8))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 9))))
(assert (= (___z3z___ (- 9)) (= (___z5z___ (- 9)) (___z4z___ (- 9)))))
(assert (= (= (___z6z___ (- 9)) 5) (___z4z___ (- 9))))
(assert (= (___z5z___ (- 9)) (and (___z7z___ (- 9)) (___z9z___ (- 9)))))
(assert (let ((?v_0 (___z6z___ (- 10)))) (= (___z6z___ (- 9)) (ite (= _base (- 9)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 9)))) (= (___z7z___ (- 9)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 10))))))))
(assert (let ((?v_0 (= _base (- 9))) (?v_1 (___z7z___ (- 10))) (?v_2 (___z8z___ (- 10)))) (= (___z8z___ (- 9)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 10)))))))))))
(assert (let ((?v_0 (= _base (- 9))) (?v_1 (___z7z___ (- 10)))) (= (___z9z___ (- 9)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 10))) (and (not ?v_1) (___z9z___ (- 10)))))))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 7)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 7)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 7) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 7))) (?v_0 (= (+ _n (* (- 1) _base)) 7))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 9))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z3z___ (- 10)))
(push 1)
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 8) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (let ((?v_0 (+ _n (- 9)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 9)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 9)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 9)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 9) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 9))) (?v_0 (= (+ _n (* (- 1) _base)) 9))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 9))) (?v_0 (= (+ _n (* (- 1) _base)) 9))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 9))) (?v_0 (= (+ _n (* (- 1) _base)) 9))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(assert (not (or (___z3z___ _n) (not (= _base (- 9))))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z3z___ (+ _n (- 10))))
(assert (= (___z3z___ (- 10)) (= (___z5z___ (- 10)) (___z4z___ (- 10)))))
(assert (= (= (___z6z___ (- 10)) 5) (___z4z___ (- 10))))
(assert (= (___z5z___ (- 10)) (and (___z7z___ (- 10)) (___z9z___ (- 10)))))
(assert (let ((?v_0 (___z6z___ (- 11)))) (= (___z6z___ (- 10)) (ite (= _base (- 10)) 0 (ite (= ?v_0 5) 1 (+ 1 ?v_0))))))
(assert (let ((?v_0 (= _base (- 10)))) (= (___z7z___ (- 10)) (and (not ?v_0) (or ?v_0 (not (___z7z___ (- 11))))))))
(assert (let ((?v_0 (= _base (- 10))) (?v_1 (___z7z___ (- 11))) (?v_2 (___z8z___ (- 11)))) (= (___z8z___ (- 10)) (and (not ?v_0) (or ?v_0 (or (and (not ?v_1) ?v_2) (and ?v_1 (and (not ?v_2) (not (___z9z___ (- 11)))))))))))
(assert (let ((?v_0 (= _base (- 10))) (?v_1 (___z7z___ (- 11)))) (= (___z9z___ (- 10)) (and (not ?v_0) (or ?v_0 (or (and ?v_1 (___z8z___ (- 11))) (and (not ?v_1) (___z9z___ (- 11)))))))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z3z___ ?v_0) (= (___z5z___ ?v_0) (___z4z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z4z___ ?v_0) (= (___z6z___ ?v_0) 5))))
(assert (let ((?v_0 (+ _n (- 8)))) (= (___z5z___ ?v_0) (and (___z9z___ ?v_0) (___z7z___ ?v_0)))))
(assert (let ((?v_0 (+ _n (- 8)))) (let ((?v_1 (___z6z___ (+ (- 1) ?v_0)))) (= (___z6z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 8) 0 (ite (= ?v_1 5) 1 (+ 1 ?v_1)))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (= (___z7z___ ?v_1) (and (not ?v_0) (or ?v_0 (not (___z7z___ (+ (- 1) ?v_1))))))))
(assert (let ((?v_4 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_1 (+ (- 1) ?v_4))) (let ((?v_2 (___z7z___ ?v_1)) (?v_3 (___z8z___ ?v_1))) (= (and (not ?v_0) (or ?v_0 (or (and (not ?v_2) ?v_3) (and ?v_2 (and (not ?v_3) (not (___z9z___ ?v_1))))))) (___z8z___ ?v_4))))))
(assert (let ((?v_1 (+ _n (- 8))) (?v_0 (= (+ _n (* (- 1) _base)) 8))) (let ((?v_2 (+ (- 1) ?v_1))) (let ((?v_3 (___z7z___ ?v_2))) (= (___z9z___ ?v_1) (and (not ?v_0) (or ?v_0 (or (and ?v_3 (___z8z___ ?v_2)) (and (not ?v_3) (___z9z___ ?v_2))))))))))
(push 1)
(assert (not (or (___z3z___ 0) (not (= _base (- 10))))))
(assert true)
(set-info :status sat)
(check-sat)
(exit)
